About Me
UPDATE: As of Fall 2017, I am teaching computer science independently through my company, Calculemus!
I taught computer science at Carnegie Mellon from 2012-2016, first as a postdoc, and then as an Assistant Teaching Professor. In 2016, I moved to Raleigh, North Carolina, where my spouse Chris Martens is a tenure-track professor, and worked for LogicBlox before starting my own business, Calculemus, to teach computer science fundamentals to new audiences.
In October 2012, I defended my dissertation and graduated with a Ph.D. from the Computer Science Department of the School of Computer Science at Carnegie Mellon University, advised by Frank Pfenning. I was also an editor for the Association for Computational Machinery's student magazine, you can see the articles I have written for XRDS.
I was an undergraduate at Princeton University in the Computer Science Department. I was fortunate as an undergraduate to be advised in independent work by Andrew Appel my junior year and by David Walker my senior year.
In the summers of 2007 and 2011, I worked on the with the Rigorous Software Engineering at MSR India in Bangalore with these guys, in particular Aditya Nori and Sriram Rajamani.
Linky partial list of things I am interested in: Twelf, its educational little sibling-elf SASyLF, and its precociously baby-sibling-elf Celf. Other educational languages like C0, the concert reading group, running, and traveling.
Research Interests
I am interested in the applications of structural proof theory and type theory. By far the most famous application of proof theory is that, by the Curry-Howard Correspondence, writing proofs can be understood as the same activity as programming, making functional programming one of the most important applications of proof theory.
Another application of proof theory is called logical frameworks. This is the practice of using logic as a language in which we describe the structure of things that we're interested in: the static and dynamic semantics of a programming language, a security protocol, a graph algorithm. But you always need the right tool for the job: my thesis work is on using a family of logics (substructural logics) as the foundation for a logical framework that can elegantly encode properties of stateful and concurrent programming languages.
Another (closely related) application of structural proof theory is logic programming. I take the viewpoint that logic programming can and should be understood as a uniform proof search strategy in a particular logic (a view that is not shared by everyone). This view makes logic programming an excellent domain-specific language for a variety of potential applications. I have written about using logic programming as a declarative specification of dynamic programming algorithms, greedy algorithms, and distributed database programming. You can also use logic programming to implement the aforementioned programming languages, security protocols, etc. that you encoded in a logical framework.
(In a slightly different direction, I am also interested in static program analysis: by treating programs as mathematical objects, we can design systems that reason about their behavior.)